The present invention relates to the field of computer-aided design of integrated circuits, and in particular, to symbolic representation of digital logic circuits.
The increase in the complexity of integrated circuits has made it imperative to verify design correctness prior to fabrication. The verification of design correctness, prior to fabrication, is essential because any design flaw detected after fabrication can have a severe economic impact in terms of increased time-to-market and reduced profit margins.
One of the basic steps involved in computer-aided design of integrated circuits is the symbolic representation of the digital logic circuit. This symbolic representation of the circuit finds several applications, such as verification of design correctness. The two methods used for verifying design correctness are model checking and equivalence checking.
Model checking is used to check the correctness of a circuit design by checking if the circuit model conforms to all properties and requirements of the circuit. Here, the desired functionality of a circuit is expressed as a collection of properties or specifications, and possibly as a model. Equivalence checking is used to verify a circuit design by checking the design against a standard design that performs the same function. Equivalence checking ascertains whether the two circuits are equivalent, i.e., they result in the same outputs for a given set of inputs. If an equivalence checker determines that the outputs of the two circuits are the same for a given set of inputs, then the two circuits are termed equivalent to one another. Model checking and equivalence checking require representing the circuits symbolically, and subsequently using these symbolic representations for checking the correctness of a model and equivalence of the two circuits.
Circuits can be classified into two categories: combinational circuits and sequential circuits. A combinational circuit is a circuit in which the output depends entirely on the values of the current inputs to the circuit. A simple example of a combinational circuit is a series of interconnected AND gates, in which none of the outputs is fed back to the AND gates.
A sequential circuit is a circuit, the output of which depends on the previous input/output values of the circuit objects, in addition to the current input values. Therefore, a sequential circuit comprises one or more combinational circuits, wherein, the output values may be fed back to the combinational circuits via storage elements. The storage elements may be implemented using flip-flops, latches, or registers.
There exist many equivalence checking techniques and tools for equivalence checking in combinational circuits. The research paper titled ‘Equivalence Checking Using Cuts and Heaps’, by Andreas Kuehlmann and Florian Krohm, Annual ACM IEEE Design Automation Conference, 34th annual conference, volume 00, pages 263-268, Published in 1997 describes one such approach. Another technique is described in the research paper titled ‘Combinational Equivalence Checking through Function Transformation’, by Hee Hwan Kwak, InHo Moon, James H. Kukula, and Thomas R. Shiple, 2002 International Conference on Computer-Aided Design (ICCAD '02), November 2002, pages 526-533.
Equivalence checking in the case of sequential circuits is relatively complex. This is because of the presence of storage elements, which are responsible for generating different sets of output values for the same set of input values. The storage elements are triggered by the clock(s) associated with the circuit; and because of the sequential nature of computation, the final output is derived after a cycle(s) of the clock(s).
The same logic can be implemented using multiple circuit designs, and each circuit design may give outputs at different clock cycles, for example, one circuit may give an output in two cycles and another circuit may give an output in three cycles.
Methods of equivalence checking often involve converting the sequential circuits to equivalent combinational circuits and then performing the equivalence check. A common method of converting sequential circuits to combinational circuits is unrolling the circuits in time and representing them in space. This is also called machine acceleration.
Machine acceleration requires replicating the netlist corresponding to the sequential circuit, i.e., the objects of the netlist (edges and nodes) are replicated in the unrolling step. The unrolled version of a circuit represented in FIG. 1 is illustrated in FIG. 3. In this case, unrolling has resulted in multiple replications (three in this case) of the associated objects and information. Machine acceleration, therefore, increases the memory requirements of the system. Further, memory requirements increase with the complexity and size of the circuits.
FIG. 1 shows a circuit diagram of a logic circuit. This circuit implements the following logic:O0=0;
For i=0 to 2, Oi=Ci+(Oi−1+Ai)
The circuit comprises two adders—adder 101 and adder 103—and a register 105. This circuit is controlled by a single clock that guides register 105. Register 105 functions as a memory element and stores the values that are output from adder 103. Register 105 is positive-edge triggered. Updating values stored by register 105 requires a trigger from the associated clock, i.e., a value will be stored in register 105 for one cycle of the clock, in the next cycle this value will be provided as an output and the stored value will be replaced by another value.
Signals A and C represent the primary inputs to the circuit. Signal A is a primary input for adder 101 and signal C is a primary input for adder 103. Register 105 stores the output of adder 103. The initial value stored in register 105 is O0=0.
The circuit represented in FIG. 1 implements the underlying logic in three cycles of the associated clock. This has been further illustrated with the help of a timing diagram, which is represented in FIG. 2.
The circuit represented in FIG. 1 performs the following sequence of events:
First Cycle
Step 1: During the first cycle, the value stored in register 105 is O0=0. In step 1, adder 101 adds external input A0 and the initial value (O0=0) stored in register 105 and gives output ‘A0+O0’;
Step 2: Adder 103 takes the output of adder 101 and C0 as input and adds them to give output ‘A0+O0+C0’;
Second Cycle
Step 3: In the second cycle of the clock, the value stored in register 105 is updated and replaced by the output of adder 103, i.e., ‘A0+O0+C0’;
Step 4: Adder 101 adds the value stored in register 105, i.e., ‘A0+O0+C0’ and another external input A1 and gives output ‘A0+O0+C0+A1’;
Step 5: Adder 103 takes the output of adder 101, i.e., ‘A0+O0+C0+A1’ and C1 as input and adds them to give output ‘A0+O0+C0+A1+C1’;
Third Cycle
Step 6: In the third cycle of the clock, the value stored in register 105 is updated and replaced by the output of adder 103, i.e., ‘A0+O0+C0+A1+C1’;
Step 7: Adder 101 adds the value stored in register 105, i.e., ‘A0+O0+C0+A1+C1’ and another external input A2 and gives output ‘A0+O0+C0+A1+C1+A2’; and
Step 8: Adder 103 takes the output of adder 101, i.e., ‘A0+O0+C0+A1+C1+A2’ and C2 as input and adds them to give the final output O, which is equal to ‘A0+O0+C0+A1+C1+A2+C2’.
Therefore, in the first cycle of the clock, step 1 and step 2 will take place; in the second cycle, step 3, step 4 and step 5 will take place; and in cycle 3, step 6, step 7 and step 8 will take place.
The same logic:O0=0;
For i=0 to 2, Oi=Ci+(Oi−1+Ai) can be implemented by a different circuit (a circuit configured in a different manner), which may require different number of clock cycles to complete the computation.
The comparison of two such circuits involves unrolling the circuits in time and representing them in space. In circuit unrolling, a circuit is represented such that it implements the underlying logic in one clock cycle. Two circuits can be compared by first unrolling them and then comparing their outputs for a given set of inputs.
FIG. 3 illustrates an unrolled version of the circuit represented in FIG. 1. The circuit represented in FIG. 3 computes the function in one cycle, which is computed by the circuit represented by FIG. 1 in three cycles.
Unrolling of a circuit results in the replication of the associated information (for example, each adder has been replicated three times in the unrolled version of the circuit), thereby increasing the number of elements in the unrolled circuit. Because of the replication of information, the memory size required to store the unrolled circuit configuration increases. Further, the memory requirements increase with the complexity and size of the circuits.
As described above, the circuit shown in FIG. 1 is controlled by a single clock. The clock guides register 105. Such circuit designs, each of which is guided by a single clock, are called single-clock-domain designs. Circuit designs, each of which is guided by multiple clocks, are called multi-clock-domain designs. In such circuits, different elements may be guided by different asynchronous clocks. For example, consider a serializer/deserializer (SERDES) that provides input to a chip. The SERDES provides input to the chip along with the clock. This clock, in all likelihood, will be asynchronous to the clock used in the chip at the consumer end. To capture the input, the chip comprises a logic that synchronizes the input to the chip's clock. This logic is guided by both the clocks, i.e., the clock of the SERDES and the clock of the chip design. In other words, this logic works on an asynchronous multi-clock-domain design. Asynchronous multi-clock-domain designs are used in many other real life situations, for example, two communicating circuits, such as routers.
The symbolic simulation of multi-clock domain designs poses many problems. Conventional methods of symbolic representation for multi-clock-domain designs include steps for converting the circuit to an equivalent single-clock-domain design. This is only possible under the following restrictions:
The period of all the clocks have to be a multiple of the period of the fastest clock in the design; and the active edge of all the clocks should coincide with the rising/falling edge of the fastest clock.
In certain cases, such as the above examples (containing asynchronous clocks), these restrictions are not fulfilled.
In light of the above discussion, there is a need for a method and a system that reduces memory requirements for representing circuit designs for different applications, such as design verification (equivalence checking, model checking, etc.). In addition, a method and a system that is capable of symbolically representing multi-clock-domain designs is required.